(include-book "../../src/acl2/cell")
(include-book "../../src/acl2/grid")
(include-book "doublecheck" :dir :teachpacks)
;;;Data Generators for grid objects used in property tests

;;Helper function used to generate a row in a lifelike grid
;;This generates elements between 0 and size-y with probability
;;density.
(defrandom random-lifelike-grid-row (size-y density)
    (let* ((rnd-num (random-between 0 100))
           (is-on (>= (* 100 density) rnd-num))
           (prev-value (if (> size-y -10)
                            (random-lifelike-grid-row (1- size-y) density)
                            (empty-tree))))
        (if is-on
            (avl-insert prev-value size-y t)
            prev-value)))

;;Generate a lifelike grid with some populated cells
;;between (0, 0) and (size-x, size-y), where each cell
;;in the range has a probability equal to density of
;;being populated. Density should be between 0 and 1.
(defrandom random-lifelike-grid (size-x size-y density)
    (let* ((prev-value (if (> size-x -10)
                        (random-lifelike-grid (1- size-x) 
                            size-y density)
                        (empty-lifelike-grid))))
        (avl-insert prev-value size-x (random-lifelike-grid-row size-y density))))

;;Generate an elementary grid with elements between
;;0 and size with probability density.
(defrandom random-elementary-grid (size density)
    ;Because an elementary grid is like one row of 
    ;a lifelike grid, we can "cheat" and reuse our
    ;random-lifelike-grid-row function
    (random-lifelike-grid-row size density))


;;Generate a random cell: simply a pair
;;of random integers that indicate a cell
(defrandom random-cell ()
    (cell (random-integer) (random-integer)))

;;Generate a random lifelike grid changeset:
;;a list of random cells
(defrandom random-lifelike-grid-changeset ()
    (random-list-of (random-cell)))

;;Generate a random elementary grid changeset:
;;a list of random integers, since elementary
;;grids are one-dimensional.
(defrandom random-elementary-grid-changeset ()
    (random-list-of (random-integer)))


(defrandom random-bool ()
    (equal (random-between 0 1) 1))